mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a

Tactic:
by
  convert! bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) using 2
  simp_rw [succ_le_iff]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ ω ≤ a.ord ↔ ℵ₀ ≤ a

Tactic:
by
  rw [← ord_aleph0, ord_le_ord]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ a.ord ≤ ω ↔ a ≤ ℵ₀

Tactic:
by
  rw [← ord_aleph0, ord_le_ord]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
h : a ≠ 0
⊢ a / a = 1

Tactic:
simpa only [mul_one] using mul_div_cancel 1 h

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x * y + z - x * y - x * (z / x) = z % x

pp: case inr.b0
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x ≠ 0

Tactic:
add_sub_cancel,

Goal state after:
case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ z - x * (z / x) = z % x

case inr.b0
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x ≠ 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0

Tactic:
exact nfpFamily_fp H 0

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case right
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ (u + log b v + 1)

Tactic:
· grw [hw, ← mul_add_one, add_assoc, opow_add]
      gcongr
      rw [add_one_le_iff]
      exact lt_opow_succ_log_self hb _

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0

Tactic:
rw [← div_add_mod b (a ^ ω), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega0,
      add_left_cancel_iff] at hab

Goal state after:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case h
a : Ordinal.{u_1}
ha' : ω ≤ preOmega a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a

Tactic:
rw [omega0_le_preOmega_iff] at ha'

Goal state after:
case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ deriv (fun x ↦ a * x) (succ c) = a ^ ω * succ c

Tactic:
deriv_succ,

Goal state after:
case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ nfp (fun x ↦ a * x) (succ (deriv (fun x ↦ a * x) c)) = a ^ ω * succ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ ℵ₀ ≤ o.cof

Tactic:
rwa [aleph0_le_cof_iff, one_lt_cof_iff]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ¬1 < m

Tactic:
apply fun h2b => ne_of_gt _ h

Goal state after:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n < n * m
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
⊢ (⨆ i, f i) + c ≤ ⨆ i, f i + c

Tactic:
obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀

Goal state after:
case inl
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ⨆ i, f i < ℵ₀
⊢ (⨆ i, f i) + c ≤ ⨆ i, f i + c

case inr
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ (⨆ i, f i) + c ≤ ⨆ i, f i + c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
hf : BddAbove (range f)
g : ι' → Cardinal.{v}
hg : BddAbove (range g)
⊢ (⨆ i, f i) + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j

Tactic:
Cardinal.ciSup_add f hf,

Goal state after:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
hf : BddAbove (range f)
g : ι' → Cardinal.{v}
hg : BddAbove (range g)
⊢ ⨆ i, f i + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case pos
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

Tactic:
obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀

Goal state after:
case pos.inl
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
hs : ⨆ i, f i < ℵ₀
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

case pos.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : ↑(Iio o) → Ordinal.{u_1}
hι : Cardinal.lift.{?u.27, u_1} o.card ≤ Cardinal.lift.{?u.27, u_1} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
simpa using card_iSup_Iio_le_of_lift hι hf

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_1
o : Ordinal.{u}
⊢ 1 ≤ (succ o).cof.ord

Tactic:
cof_succ,

Goal state after:
case refine_1
o : Ordinal.{u}
⊢ 1 ≤ ord 1
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl
b : Ordinal.{u_1}
n : ℕ
⊢ (↑n ^ b).card ≤ max ℵ₀ (max (↑n).card b.card)

Tactic:
obtain ⟨m, rfl⟩ | hb := eq_natCast_or_omega0_le b

Goal state after:
case inl.inl
n m : ℕ
⊢ (↑n ^ ↑m).card ≤ max ℵ₀ (max (↑n).card (↑m).card)

case inl.inr
b : Ordinal.{u_1}
n : ℕ
hb : ω ≤ b
⊢ (↑n ^ b).card ≤ max ℵ₀ (max (↑n).card b.card)
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ ℵ₀ ≤ o.cof

Tactic:
rwa [aleph0_le_cof_iff, one_lt_cof_iff]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ iSup f < c.ord

Tactic:
by
  apply Ordinal.lift_iSup_lt_of_lt_cof _ hf
  rwa [lift_umax, Ordinal.lift_id', hc.cof_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Infinite α
f : α → Bool
x : α × Bool
⊢ (fun x ↦ (x.1, f x.1 ^^ x.2)) ((fun x ↦ (x.1, f x.1 ^^ x.2)) x) = x

Tactic:
simp_rw [← Bool.xor_assoc, Bool.xor_self, Bool.false_xor]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ Nonempty (α ≃ α ⊕ β')

Tactic:
← lift_mk_eq',

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{max u v, u} #α = lift.{u, max u v} #(α ⊕ β')
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ Nonempty (α ≃ α ⊕ β')

Tactic:
simp_rw [← lift_mk_eq', mk_sum, lift_add, lift_lift]

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{max u v, u} #α = lift.{max v u, u} #α + lift.{u, v} #β'
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
← lift_mk_eq',

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{v, u} #↑sᶜ = lift.{u, v} #↑(range ⇑f)ᶜ
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ i ∈ f.splitSupport.val ∨ f.split i = 0

Tactic:
by
          rw [← Finset.mem_def, mem_splitSupport_iff_nonzero]
          exact (em _).symm

Goal state after:
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ (single j x) j' = (single ⟨i, j⟩ x) ⟨i, j'⟩

Tactic:
rw [single_eq_of_ne hj, single_eq_of_ne]

Goal state after:
case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ ⟨i, j'⟩ ≠ ⟨i, j⟩
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
this : ∏ i ∈ v.support, f i (v i) = ∏ i, f i (v i)
⊢ v.prod f = ∏ i, f i (equivFunOnFintype v i)

Tactic:
by simp [DFinsupp.prod, this]

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case refine_1
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sx.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0

Tactic:
intro i H1 H2

Goal state after:
case refine_1
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1✝ : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2✝ : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx.toFinset
H2 : i ∉ sx.toFinset ∩ sy.toFinset
⊢ (φ i) (f i) = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case refine_3
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sy.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0

Tactic:
intro i H1 H2

Goal state after:
case refine_3
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1✝ : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2✝ : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy.toFinset
H2 : i ∉ sx.toFinset ∩ sy.toFinset
⊢ (φ i) (f i) = 0
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : SMul S R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : Module S M
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S R P
inst✝³ : AddCommMonoid M'
inst✝² : Module S M'
inst✝¹ : AddCommMonoid P'
inst✝ : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective ⇑k
f : M →ₗ[R] P
hf : ∀ (m : M'), f (i m) ∈ k.range
m : M'
⊢ (i.restrictScalarsRange k hk f hf) m = 0 ↔ f (i m) = 0

Tactic:
rw [← hk.eq_iff, restrictScalarsRange_apply, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔ ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
simp_rw [iSupIndep_def, Submodule.disjoint_def]
  constructor
  · intro h s v hv hv0 i hi
    apply h _ _ (hv i hi)
    rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0
    rw [← Submodule.neg_mem_iff, hv0]
    exact SetLike.le_def.mp (biSup_mono <| by grind) (Submodule.sum_mem_biSup <| by grind)
  · intro h i x hx hsup
    obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup
    contrapose! h
    use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j
    refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
    · beta_reduce
      split_ifs with h
      · exact (p j).neg_mem (h ▸ hx)
      · simpa [h] using hf j
    · specialize hf i
      simp at hf
      grind [Finsupp.sum, Finset.sum_congr]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
s : Set M
h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' s))
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' s)

Tactic:
let s' := @Submonoid.closure (Multiplicative M) Multiplicative.mulOneClass s

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
s : Set M
h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' s))
s' : Submonoid (Multiplicative M) := Submonoid.closure s
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' s)
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ [].prod ↔ ∃ f, [].prod = a

Tactic:
List.prod_nil,

Goal state after:
case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ 1 ↔ ∃ f, 1 = a
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case h.mp
α : Type u_1
inst✝ : Monoid α
n : ℕ
f : Fin n → Set α
fi : (i : Fin n) → ↑(f i)
⊢ ∃ x, (List.ofFn ((fun x ↦ ↑x.snd) ∘ x)).prod = (List.ofFn fun i ↦ ↑(fi i)).prod ∧ Sigma.fst ∘ x = f

Tactic:
exact ⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
hf : Injective f
x y : R[N]
⊢ comapDomain f hf (x + y) = comapDomain f hf x + comapDomain f hf y

Tactic:
ext; simp [comapDomain_add_of_injective hf]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
⊢ f = g

Tactic:
by
  have : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom :=
    Finsupp.addHom_ext h
  convert congr(($this).comp coeffAddEquiv.toAddMonoidHom) <;> ext <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
u : Finset V
h : ↑u ⊆ s ∪ ↑({x ∈ t | x ∉ s}) ∧ s ⊆ ↑u ∧ u.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card
⊢ s ∪ ↑({x ∈ t | x ∉ s}) ⊆ s ∪ ↑t

Tactic:
simp +contextual [subset_def, or_imp]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
⊢ UniqueMul A B a0 b0 ↔ #({p ∈ A ×ˢ B | p.1 * p.2 = a0 * b0}) ≤ 1

Tactic:
simp_rw [card_le_one_iff, mem_filter, mem_product]

Goal state after:
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
⊢ UniqueMul A B a0 b0 ↔
    ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
obtain ⟨p, hp, _, _, _, hu, _⟩ := h (Nat.one_lt_mul_iff.mpr ⟨hA, hB, hc⟩)

Goal state after:
case neg
G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
p : G × G
hp : p ∈ A ×ˢ B
w✝ : G × G
left✝¹ : w✝ ∈ A ×ˢ B
left✝ : p ≠ w✝
hu : UniqueMul A B p.1 p.2
right✝ : UniqueMul A B w✝.1 w✝.2
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : k ≤ #s
a : Fin k
⊢ (s.orderEmbOfCardLe h) a ∈ s

Tactic:
by
  simp only [orderEmbOfCardLe, RelEmbedding.coe_trans, Finset.orderEmbOfFin_mem,
    Function.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ #(s ^ n) ≤ #(s ^ n * s)

Tactic:
exact card_le_card_mul_right hs

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = (monomial n) 1 * (monomial 1) 1

Tactic:
monomial_mul_monomial,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = (monomial (n + 1)) (1 * 1)
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ M ≤ pi s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom i) (L i)

Tactic:
by simp [SetLike.le_def]; grind

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * (monomial 1) 1 = (monomial (n + 1)) r

Tactic:
monomial_mul_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial (n + 1)) (r * 1) = (monomial (n + 1)) r
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k n : ℕ
r : R
⊢ X ^ k * (monomial n) r = (monomial (n + k)) r

Tactic:
rw [X_pow_mul, monomial_mul_X_pow]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ (monomial n) a * (monomial 1) 1 = (monomial (n + 1)) a

Tactic:
monomial_mul_monomial,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ (monomial (n + 1)) (a * 1) = (monomial (n + 1)) a
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint p q

Tactic:
by
  rw [disjoint_iff, disjoint_iff, Sublattice.mk_inf_mk,
    Subtype.mk_eq_bot_iff (⊥ : f.invtSubmodule).property]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : ↥p
⊢ (p.projection q hpq) ↑x = ↑x

Tactic:
simp [projection]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
htop : ⨆ i, f i = ⊤
i : ι
hi : ↑d < f i
⊢ False

Tactic:
exact (((h i).trans_lt hi).trans_le (ENat.self_le_mul_left _ hne)).false

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case mpr.mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₁ : M₁
⊢ τ₃ (g (f x₁)) = τ₃ 1

Tactic:
simp only [← comm₁₂, ← comm₂₃, h.apply_apply_eq_one (τ₁ x₁), map_one]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr.inl
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb hb0 : b ∈ B
he0 : a0 * b = (A * B).max' ⋯
he : a * b = a0 * b
⊢ a = a0 ∧ b = b

Tactic:
exact ⟨mul_right_cancel he, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2.inr.inl
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb hb1 : b ∈ B
he1 : a1 * b = (A * B).min' ⋯
he : a * b = (a1, b).1 * (a1, b).2
⊢ a = (a1, b).1 ∧ b = (a1, b).2

Tactic:
exact ⟨mul_right_cancel he, rfl⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ p_1, ⨆ (_ : RelSeries.last p_1 = (RelSeries.eraseLast p).last), ↑p_1.length + 1

Tactic:
apply le_iSup₂_of_le p.eraseLast (by rfl) (by simp [hlen])

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a

Tactic:
suffices ∃ x < a, ↑n ≤ height x by
      simp_all [minimal_iff_forall_lt]
    simp only [top_le_iff, height_eq_top_iff] at hfin
    obtain ⟨p, rfl, hp⟩ := hfin (n + 1)
    use p.eraseLast.last, p.eraseLast_last_rel_last (by lia)
    simpa [hp] using length_le_height_last (p := p.eraseLast)

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
m : M
hm : ∃ b, m + b = 0
n : N
b : M
eq : m + b = 0
⊢ ∃ b, m ⊗ₜ[R] n + b = 0

Tactic:
exact ⟨b ⊗ₜ[R] n, by rw [← add_tmul, eq, zero_tmul]⟩

Goal state after: