mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind
c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c * c ≤ c

Tactic:
induction c using Cardinal.inductionOn with | mk α
   =>  _ 

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
⊢ #α * #α ≤ #α
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u}
h : a ≠ 0
⊢ IsLeast {b | a - b < a} (ω ^ log ω a)

Tactic:
by
  refine ⟨sub_omega0_opow_log_lt h, fun c (hc : a - _ < _) ↦ ?_⟩
  contrapose! hc
  exact le_sub_of_add_le (add_of_omega0_opow_le hc (opow_log_le_self ω h)).le

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof < ℵ₀ ↔ o.cof ≤ 1

Tactic:
simpa using Order.cof_lt_aleph0_iff (α := o.ToType)

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

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b = 1 ∨ a = 0

Tactic:
have hb : b ≠ 0 := by
      rintro rfl
      apply h2a
      rw [mul_zero] at h
      exact h.symm

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1 ∨ a = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ lift.{v, u} o ≤ ω_ 1 ↔ o ≤ ω_ 1

Tactic:
simpa using lift_le (b := ω₁)

Goal state after:
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.add_ciSup g hg

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

Goal state before:
pp: case refine_1
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
x : β
hx : x ∈ s
h✝ : f ⟨x, hx⟩ = a
⊢ x ∈ s

Tactic:
exact hx

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c < c ^ c.ord.cof

Tactic:
induction c using Cardinal.inductionOn with | mk α
   =>  _ 

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
⊢ #α < #α ^ (#α).ord.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{v, u} #α = lift.{u, v} #β
h2 : lift.{v, u} #↑s = lift.{u, v} #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
⊢ lift.{v, u} #↑sᶜ = lift.{u, v} #↑tᶜ

Tactic:
replace h1 : Fintype.card α = Fintype.card β := (Fintype.ofEquiv_card _).symm

Goal state after:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h2 : lift.{v, u} #↑s = lift.{u, v} #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
⊢ lift.{v, u} #↑sᶜ = lift.{u, v} #↑tᶜ
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Nontrivial R
inst✝¹ : Module R M
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ

Tactic:
let Φ := fun k : κ => (b.repr (v k)).support

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Nontrivial R
inst✝¹ : Module R M
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ
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 : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
hj : j' ≠ j
⊢ (single ⟨i, j⟩ x) ⟨i, j'⟩ = (single j x) j'

Tactic:
single_eq_of_ne,

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

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

Goal state before:
pp: ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ (mk g.support fun i ↦ f (↑i) (g ↑i)).prod h = g.prod fun i b ↦ h i (f i b)

Tactic:
refine (Finset.prod_subset support_mk_subset ?_).trans ?_

Goal state after:
case refine_1
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ ∀ x ∈ g.support, x ∉ (mk g.support fun i ↦ f (↑i) (g ↑i)).support → h x ((mk g.support fun i ↦ f (↑i) (g ↑i)) x) = 1

case refine_2
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ ∏ x ∈ g.support, h x ((mk g.support fun i ↦ f (↑i) (g ↑i)) x) = g.prod fun i b ↦ h i (f i b)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case some
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
⊢ ((fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f)) (some i) = f (some i)

Tactic:
rw [extendWith_some, comapDomain_apply]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = ((Dual.eval R M) ((evalEquiv R M).symm g)) f

Tactic:
Dual.eval_apply

Goal state after:
R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = f ((evalEquiv R M).symm g)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p).range ≤ ⨆ i, ⨆ (_ : p i), S i

Tactic:
rintro x ⟨v, rfl⟩
    refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
    refine mem_iSup_of_mem i ?_
    by_cases hp : p i
    · simp [hp]
    · simp [hp]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h]
  nth_rw 4 [add_comm]
  simp only [add_assoc]
  congr! 2
  rw [add_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R v

Tactic:
classical
  rw [linearIndependent_iff]
  intro l hl
  let a :=
    DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
      l.toDFinsupp
  have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
  ext i
  apply smul_left_injective R (hv' i)
  have : l i • v i = a i := rfl
  simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
  simpa

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
⊢ support 0 = ∅

Tactic:
simp only [support, Finsupp.support_zero, map_zero]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
φ ψ : AddChar A M
⊢ toMonoidHomEquiv.toFun (φ * ψ) = toMonoidHomEquiv.toFun φ * toMonoidHomEquiv.toFun ψ

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
φ ψ : Additive (AddChar A M)
⊢ toAddMonoidHomEquiv.toFun (φ + ψ) = toAddMonoidHomEquiv.toFun φ + toAddMonoidHomEquiv.toFun ψ

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
⊢ ψ (-a) = (ψ a)⁻¹

Tactic:
map_neg_eq_inv

Goal state after:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
⊢ (ψ a)⁻¹ = (ψ a)⁻¹
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
a : V
s : Set V
⊢ LinearIndepOn K id (insert a s) ↔ LinearIndepOn K id s ∧ (a ∈ span K s → a ∈ s)

Tactic:
by
  simpa using linearIndepOn_insert_iff (a := a) (f := id)

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
x : R[N]
hx : ↑x.coeff.support ⊆ Set.range f
hf : Injective f
⊢ mapDomain f (comapDomain f hf x) = x

Tactic:
by
  ext : 1; exact Finsupp.mapDomain_comapDomain _ hf _ hx

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Mul M
⊢ ∀ (a b c : R[M]), (a + b) * c = a * c + b * c

Tactic:
simp [mul_def, add_mul, sum_add, sum_add_index]

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
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
⊢ ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) (x✝¹ * x✝) =
    ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) x✝¹ *
      ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) x✝

Tactic:
by rfl

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
hz : 0 < k
⊢ (s.orderEmbOfFin h) ⟨k - 1, ⋯⟩ = s.max' ⋯

Tactic:
by
  simp [orderEmbOfFin_apply, max'_eq_sorted_last, h]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
⊢ b1 * (a1 * (b2 * a2)) = b1 * a1 * (b2 * a2)

Tactic:
← mul_assoc b1

Goal state after:
G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
b2 : G
hb2 : b2 ∈ B
a2 : G
ha2 : a2 ∈ A
h2 : b2 * a2 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) (b2 * a2)
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a1 * b2
⊢ b1 * a1 * (b2 * a2) = b1 * a1 * (b2 * a2)
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ (Set.range fun x ↦ single (u x) 1) ⊆ ↑(lmapDomain R R u).range

Tactic:
Set.range_subset_iff

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ ∀ (y : α), single (u y) 1 ∈ ↑(lmapDomain R R u).range
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case add
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : α →₀ M
f_in : f ∈ span R {x | ∃ i x_1, single i x_1 = x}
g_in : g ∈ span R {x | ∃ i x_1, single i x_1 = x}
⊢ f + g ∈ span R {x | ∃ i x_1, single i x_1 = x}

Tactic:
| add f g f_in g_in =>

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ ⇑((lsum R) fun x ↦ f x • φ) '' {x | ∃ i x_1, single i x_1 = x} = Set.range f • ⇑φ '' univ

Tactic:
aesop (add simp Set.mem_smul)

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
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔
    ↑((p.prodEquivOfIsCompl q h).symm x).1 + ↑((p.prodEquivOfIsCompl q h).symm x).2 ∈ q

Tactic:
Submodule.add_mem_iff_left _ (Submodule.coe_mem _),

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ ↑((p.prodEquivOfIsCompl q h).symm x).1 ∈ q
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
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : E →ₗ[R₁] F
x : E
⊢ ((ofIsComplProd h).toFun ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) φ)) x = φ x

Tactic:
obtain ⟨a, b, hab, _⟩ := existsUnique_add_of_isCompl h x

Goal state after:
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : E →ₗ[R₁] F
x : E
a : ↥p
b : ↥q
hab : ↑a + ↑b = x
right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = x → r = a ∧ s = b
⊢ ((ofIsComplProd h).toFun ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) φ)) x = φ x
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
simp_rw [iSup_add, add_iSup]; exact iSup₂_le h

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ (∃! f, Function.graph f = R) ↔ ∀ (a : α), ∃! b, (a, b) ∈ R

Tactic:
by
  constructor
  · rintro ⟨f, rfl, _⟩ x
    simp
  intro h
  choose f hf using fun x ↦ (h x).exists
  refine ⟨f, ?_, by aesop⟩
  ext ⟨a, b⟩
  constructor
  · aesop
  · exact (h _).unique (hf _)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
p : Submodule R M
q : Submodule R N
hm : m ∈ p
hn : n ∈ q
⊢ (f ↑⟨m, hm⟩) n = (f m) n

Tactic:
by rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.eraseLast.snoc p.last ⋯ = p

Tactic:
by
  apply toList_injective
  rw [toList_snoc, ← getLast_toList, toList_eraseLast _ h, List.dropLast_append_getLast]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

Tactic:
rw [height_le_iff]
    exact fun h p hlast => h (le_of_eq hlast)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last = (RelSeries.eraseLast p).last

Tactic:
by rfl

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ ⊥ < krullDim α ↔ Nonempty α

Tactic:
bot_lt_iff_ne_bot,

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≠ ⊥ ↔ Nonempty α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x b : α), ¬x < b) → ∀ (i : LTSeries α), ↑i.length ≤ 0

Tactic:
· rintro H ⟨_ | n, l, h⟩
    · simp
    · cases H (l 0) (l 1) (h 0)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ ↑(⨆ a, height a) = ⨆ a, ↑(height a)

Tactic:
WithBot.coe_iSup (OrderTop.bddAbove _)

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ ⨆ i, ↑(height i) = ⨆ a, ↑(height a)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ ↑(⨆ a, coheight a) = ⨆ a, ↑(coheight a)

Tactic:
WithBot.coe_iSup (OrderTop.bddAbove _)

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ ⨆ i, ↑(coheight i) = ⨆ a, ↑(coheight a)
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N : AddSubmonoid A
m : R
n : A
hm : m ∈ M
hn : n ∈ N
⊢ (DistribSMul.toAddMonoidHom A ↑⟨m, hm⟩) n = m • n

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : A
hn : n ∈ ⊥
⊢ m • n ∈ ⊥

Tactic:
by
    rw [AddSubmonoid.mem_bot] at hn ⊢; rw [hn, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ a' * b' ∈ closure (S * T)

Tactic:
exact subset_closure (Set.mul_mem_mul ha' hb')

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommGroup P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : N →ₗ[R] P
⊢ (rTensorHom Q) (-f) = -(rTensorHom Q) f

Tactic:
exact (rTensorHom (R := R) (N := N) (P := P) Q).map_neg f

Goal state after:
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime (-x + z * y) y ↔ IsCoprime x y

Tactic:
add_mul_right_left_iff,

Goal state after:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime (-x) y ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
y z : R
⊢ IsCoprime (y * z + 1) y

Tactic:
rw [mul_add_left_left_iff]

Goal state after:
R : Type u
inst✝ : CommRing R
y z : R
⊢ IsCoprime 1 y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
h : 0 ≤ x
⊢ IsCoprime |x| y ↔ IsCoprime x y

Tactic:
abs_of_nonneg h

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
h : 0 ≤ x
⊢ IsCoprime x y ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (-x + z * y) y ↔ IsRelPrime x y

Tactic:
add_mul_right_left_iff,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (-x) y ↔ IsRelPrime x y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
y z : R
⊢ IsRelPrime (y * z + 1) y

Tactic:
rw [mul_add_left_left_iff]

Goal state after:
R : Type u_1
inst✝ : CommRing R
y z : R
⊢ IsRelPrime 1 y
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h
x y : ℤ
h : IsCoprime x y
⊢ x.gcd y = 1

Tactic:
← Int.isCoprime_iff_gcd_eq_one

Goal state after:
case h
x y : ℤ
h : IsCoprime x y
⊢ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
Hs : (↑t).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ t, s i ∣ z
⊢ ∏ x ∈ t, s x ∣ z

Tactic:
by
  classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert a r har ih =>
    rw [Finset.prod_insert har]
    refine IsCoprime.mul_dvd ?_ ?_ ?_
    · refine IsCoprime.prod_right fun i hir ↦ ?_
      exact Hs (by simp) (by simp [hir]) (ne_of_mem_of_not_mem hir har).symm
    · exact Hs1 a (Finset.mem_insert_self a r)
    · refine ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi
      simp only [Finset.coe_insert, Set.subset_insert]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
⊢ span R S * span R T = span R (S * T)

Tactic:
rw [mul_eq_map₂]; apply map₂_span_span

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case refine_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
⊢ (↑t).Pairwise (IsCoprime on s)

Tactic:
rintro i hi j hj h
    apply IsCoprime.prod_right_iff.mp (hp i hi)
    exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h (Finset.mem_singleton.mp f).symm⟩

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
x : A
hx : x ∈ M ^ n
⊢ C n x hx

Tactic:
induction n generalizing x with
  | zero =>
    rw [pow_zero] at hx
    obtain ⟨r, rfl⟩ := mem_one.mp hx
    exact algebraMap r
  | succ n n_ih =>
    revert hx
    simp_rw [pow_succ]
    exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

Goal state after: