mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
⊢ LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr)) →
    LinearIndependent R v

Tactic:
rintro ⟨hl, hr, hlr⟩

Goal state after:
case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : LinearIndependent R (v ∘ Sum.inl)
hr : LinearIndependent R (v ∘ Sum.inr)
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
⊢ LinearIndependent R v
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i, n i)
b : Fin m
⊢ (↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b < n b

Tactic:
cases m

Goal state after:
case zero
ι : Type u_1
M : Type u_2
n : Fin 0 → ℕ
a : Fin (∏ i, n i)
b : Fin 0
⊢ (↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b < n b

case succ
ι : Type u_1
M : Type u_2
n✝ : ℕ
n : Fin (n✝ + 1) → ℕ
a : Fin (∏ i, n i)
b : Fin (n✝ + 1)
⊢ (↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b < n b
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑((Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm
                (Equiv.sumSigmaDistrib fun a ↦ Fin (n (finSumFinEquiv a))))
              (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i ↦ Fin (n (finSumFinEquiv (Sum.inr i))))))
            finSumFinEquiv)
          (finCongr ⋯))
        ⟨⟨iv, hi⟩, j⟩) =
    ∑ i, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd

Tactic:
unfold finSumFinEquiv

Goal state after:
case succ
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑((Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans
                { toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m), invFun := fun i ↦ Fin.addCases Sum.inl Sum.inr i,
                      left_inv := ⋯, right_inv := ⋯ }.sigmaCongrLeft.symm
                (Equiv.sumSigmaDistrib fun a ↦
                  Fin
                    (n
                      ({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                          invFun := fun i ↦ Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ }
                        a))))
              (finSigmaFinEquiv.sumCongr
                (Equiv.uniqueSigma fun i ↦
                  Fin
                    (n
                      ({ toFun := Sum.elim (Fin.castAdd 1) (Fin.natAdd m),
                          invFun := fun i ↦ Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ }
                        (Sum.inr i))))))
            { toFun := Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i, n i.castSucc)),
              invFun := fun i ↦ Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ })
          (finCongr ⋯))
        ⟨⟨iv, hi⟩, j⟩) =
    ∑ i, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
⊢ ¬LinearIndependent R v ↔ ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, 0 < f i

Tactic:
simp only [linearIndependent_iffₒₛ, pos_iff_ne_zero]
  push +distrib Not
  refine ⟨fun ⟨s, t, f, hst, heq, h⟩ => ?_,
    fun ⟨s, t, f, hst, heq, hi⟩ => ⟨s, t, f, hst, heq, .inl hi⟩⟩
  rcases h with ⟨i, hi, hfi⟩ | ⟨i, hi, hgi⟩
  · exact ⟨s, t, f, hst, heq, i, hi, hfi⟩
  · exact ⟨t, s, f, hst.symm, heq.symm, i, hi, hgi⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} #↑↑⟨range v, ⋯⟩

Tactic:
exact lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ ∀ w < 1, ∃ i, w < #↑↑i

Tactic:
intro w hw
    exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ Module.rank R M = 1

Tactic:
by
  rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]
  · have := Module.subsingleton R M
    simp [Set.subsingleton_of_subsingleton]
  · intro w hw
    exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
e : α
⊢ ↑(Fintype.card ↑{e}) = 1

Tactic:
card_singleton,

Goal state after:
α : Type u_1
e : α
⊢ ↑1 = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_sdiff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  have hle' : (s \ {a}).encard ≤ (t \ {b}).encard := by
    rwa [← ENat.add_le_add_iff_right ENat.one_ne_top,
    encard_sdiff_singleton_add_one has, encard_sdiff_singleton_add_one hbt]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.sdiff hle'
  simp only [preimage_sdiff, subset_def, mem_sdiff, mem_singleton_iff, mem_preimage, and_imp]
    at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_sdiff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  simp only [mem_sdiff, mem_singleton_iff, insert_sdiff_singleton, subset_def,
    mem_insert_iff, mem_preimage, Function.update_apply, forall_eq_or_imp, ite_true, and_imp,
    mem_image, ite_eq_left_iff, not_exists, not_and, not_forall, exists_prop, and_iff_right hbt]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case neg
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : ¬j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
simpa [H] using hs _

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑(t \ s) ≤ 0
⊢ ENat.card ↑(t \ s) = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑(t \ s) ≤ 0
⊢ ENat.card ↑(t \ s) ≤ 0
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: case neg
η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : ¬j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
simpa [H] using hs _

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ x ∈ (b.repr c).support, ∑ x_1 ∈ (b.repr d).support, (b.repr c) x • (b.repr d) x_1 • (z * b x * b x_1) =
    ∑ x ∈ (b.repr d).support, ∑ x_1 ∈ (b.repr c).support, (b.repr d) x • (b.repr c) x_1 • (z * b x_1 * b x)

Tactic:
(@SMulCommClass.smul_comm R R A)

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ x ∈ (b.repr c).support, ∑ x_1 ∈ (b.repr d).support, (b.repr c) x • (b.repr d) x_1 • (z * b x * b x_1) =
    ∑ x ∈ (b.repr d).support, ∑ x_1 ∈ (b.repr c).support, (b.repr c) x_1 • (b.repr d) x • (z * b x_1 * b x)
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
x : ↥A
i : ι
this :
  mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ ↑(addSubgroupOfClosure A b h).repr =
    (↑ℤ ↑b.repr).domRestrict (AddSubgroup.toIntSubmodule A)
⊢ ↑(((addSubgroupOfClosure A b h).repr x) i) = (b.repr ↑x) i

Tactic:
exact DFunLike.congr_fun (LinearMap.congr_fun this x) i

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
by
  simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one, Finite.mem_toFinset]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
h' : f.ker ≤ p
⊢ (p.liftQ f h).ker = ⊥

Tactic:
rw [ker_liftQ, le_antisymm h h', mkQ_map_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M × M₂ →ₗ[R] M₃
⊢ (f ∘ₗ inl R M M₂).coprod (f ∘ₗ inr R M M₂) = f

Tactic:
by
  rw [← comp_coprod, coprod_inl_inr, comp_id]

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ ↑(Ioo (pred a) b) = ↑(Ico a b)

Tactic:
simpa using Set.Ioo_pred_left_eq_Ioc_of_not_isMin ha _

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
rw [Icc_eq_cons_Ioc h, prod_cons]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ Nat.find ⋯ = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ Nat.find ⋯ ≤ 0
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
by_cases h : IsMax i

Goal state after:
case pos
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : IsMax i
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ disjointed f (succ i) ⊔ f i = f (succ i)
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ ↑(List.Nat.antidiagonal (n + 1)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)

Tactic:
List.Nat.antidiagonal_succ',

Goal state after:
n : ℕ
⊢ ↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ filter ((fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm) (map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)

Tactic:
← map_filter,

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding ({a ∈ antidiagonal n | a.2 ≤ k}) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ filter ((fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm) (map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
← map_filter,

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding ({a ∈ antidiagonal n | k ≤ a.1}) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
h : M ⊔ M' ≠ ⊤
⊢ M = M'

Tactic:
exact hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
x y : α
h : Associated x y
⊢ x ∈ I ↔ y ∈ I

Tactic:
by
  obtain ⟨u, rfl⟩ := h.symm
  exact I.mul_unit_mem_iff_mem u.isUnit

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y - z * x} = span {x, y}

Tactic:
by
  rw [mul_comm, span_pair_sub_left_mul]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : x ∈ (LinearMap.toSpanSingleton R R e).ker
⊢ x * (1 - e) = x

Tactic:
rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case isUnit_or_isUnit.refine_2
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ IsIdempotentElem (a * (c * d))

Tactic:
rw [isIdempotentElem_iff]

Goal state after:
case isUnit_or_isUnit.refine_2
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a * (c * d) * (a * (c * d)) = a * (c * d)
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ max x₁ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂

Tactic:
le_max_iff

Goal state after:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
a : α
⊢ ⋃ i, Ico (f i) a = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x

Tactic:
by
  simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ i, ⋃ (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ x < a, ∃ i, ∃ (hi : p i), f i hi ≤ x

Tactic:
by
  simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: β : Type u_2
f : Filter β
s : Set β
⊢ map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s

Tactic:
map_comap,

Goal state after:
β : Type u_2
f : Filter β
s : Set β
⊢ f ⊓ 𝓟 (range Subtype.val) = f ⊓ 𝓟 s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : range m ∈ f
⊢ map m (comap m f) = f

Tactic:
map_comap,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : range m ∈ f
⊢ f ⊓ 𝓟 (range m) = f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
s : Set α
f : Filter α
⊢ map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s

Tactic:
map_comap,

Goal state after:
α : Type u_1
s : Set α
f : Filter α
⊢ f ⊓ 𝓟 (range Subtype.val) = f ⊓ 𝓟 s
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
⊢ (iInf f).NeBot

Tactic:
cases isEmpty_or_nonempty ι
  · constructor
    simp [iInf_of_empty f, top_ne_bot]
  · exact iInf_neBot_of_directed' hd hb

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
h : lb.HasBasis pb sb
⊢ (⊤ ×ˢ lb).HasBasis pb fun x ↦ univ ×ˢ sb x

Tactic:
simpa only [principal_univ] using h.principal_prod univ

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ n s, span R (range s) = N

Tactic:
rw [fg_def]
  constructor
  · rintro ⟨S, Sfin, hS⟩
    obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
    exact ⟨n, f, hS⟩
  · rintro ⟨n, s, hs⟩
    exact ⟨range s, finite_range s, hs⟩

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s') → (span R s).FG

Tactic:
· intro ⟨s', _, h⟩
    exact ⟨s', h.symm⟩

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

Goal state before:
pp: case refine_2.a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ cof α ≤ 1

pp: case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ 1 ≤ cof α

Tactic:
· apply (cof_le (s := {t}) _).trans_eq (mk_singleton _)
      rwa [isCofinal_singleton_iff]

Goal state after:
case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ 1 ≤ cof α
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ b ∈ t, ¬Ici b ∩ t ⊆ s
hcof : IsCofinalFor t (t \ s)
x : α
hx : x ∈ t \ s
hxs : x ∈ s
⊢ False

Tactic:
exact hx.2 hxs

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{u + 1, u} c < univ.{u, u + 1}

Tactic:
by
  simpa only [Ordinal.liftPrincipalSeg_coe, lift_ord, lift_succ, ord_le, Order.succ_le_iff] using!
    le_of_lt (Ordinal.liftPrincipalSeg.{u, u + 1}.lt_top (Order.succ c).ord)

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

Goal state before:
pp: ι : Type u_3
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → Ordinal.{max u_3 u_4}
⊢ (type r).bsup (bfamilyOfFamily' r f) = iSup f

Tactic:
by
  simp +unfoldPartialApp only [← iSup'_eq_bsup r, enum_typein, familyOfBFamily', bfamilyOfFamily']

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

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ a + c / b ≤ (b * a + c) / b

Tactic:
· rw [← mul_le_iff_le_div b0, mul_add, add_le_add_iff_left]
    apply mul_div_le

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
rw [not_and_or, not_lt, Ne, not_not] at hbn

Goal state after:
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ n = 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
by_cases a = 0

Goal state after:
case pos
a b : Ordinal.{u_1}
h✝ : a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case neg
a b : Ordinal.{u_1}
h✝ : ¬a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ log b (n / b * b) = log b n

Tactic:
by
  rcases le_or_gt b 1 with hb | hb
  · rw [log_of_left_le_one hb, log_of_left_le_one hb]
  rcases lt_or_ge n b with h | h
  · rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]
  rw [log_mul_base hb (Nat.div_pos h (by lia)).ne', log_div_base,
    Nat.sub_add_cancel (succ_le_iff.2 <| log_pos hb h)]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c ≤ n ↔ c * k ≤ log b n

Tactic:
le_log_iff_pow_le hb hn,

Goal state after:
case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c ≤ n ↔ b ^ (c * k) ≤ n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x

Tactic:
opow_le_iff_le_log' hb hc

Goal state after:
case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ c ≤ log b x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o

Tactic:
rw [div_pos (opow_ne_zero _ hb.ne')]

Goal state after:
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ a < ω ^ ω ^ b ↔ ∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)

Tactic:
simp_rw [lt_omega0_opow (opow_ne_zero _ omega0_ne_zero), lt_omega0_opow hb]
  constructor
  · intro ⟨a, ⟨b, hb, ⟨m, hm⟩⟩, ⟨n, hn⟩⟩
    exact ⟨_, hb, _, hn.trans <| opow_mul_lt_opow (natCast_lt_omega0 _) <|
      hm.trans_le (mul_le_mul_right (Nat.cast_le.2 m.le_succ) _)⟩
  · intro ⟨a, ha, ⟨n, hn⟩⟩
    refine ⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩
    · simp [mul_lt_mul_iff_right₀, opow_pos]
    · simpa

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp (fun x ↦ a + x) 0 = a * ω

Tactic:
by
  simp [← iSup_iterate_eq_nfp]

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c.ord.IsInitial

Tactic:
by
  rw [IsInitial, card_ord]

Goal state after: