mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst✝ : One P
hg : 1 ∈ Set.range g
⊢ MulExact f g ↔ MulExact Subtype.val (Set.rangeFactorization g)

Tactic:
let : One (Set.range g) := ⟨⟨1, hg⟩⟩
  have : ((1 : Set.range g) : P) = 1 := rfl
  simp [MulExact, Subtype.ext_iff, this]

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
⊢ succ 0 = 1

Tactic:
by simpa using succ_natCast (α := α) 0

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

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
by
  simp_rw [biSup_add' hp, add_biSup' hq]
  exact iSup₂_le fun i hi => iSup₂_le (h i hi)

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
⊢ m = ⊥ ↔ f = 0

Tactic:
constructor <;> rintro rfl
  · ext
    simpa using hf.map_mem _
  · rw [← hf.range, range_zero]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
⊢ x ∈ List.ofFn s.toFun ↔ x ∈ s

Tactic:
List.mem_ofFn',

Goal state after:
α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
⊢ x ∈ Set.range s.toFun ↔ x ∈ s
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
hg : Surjective ⇑g
tfae_1_iff_3 : (∃ l, g ∘ₗ l = LinearMap.id) ↔ ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
⊢ (∃ l, l ∘ₗ f = LinearMap.id) ↔ ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e

Tactic:
simpa using (h.splitInjectiveEquiv hg).nonempty_congr

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ (p.tail hp).cons p.head ⋯ = p

Tactic:
apply toList_injective
  simp [← head_toList]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ Nonempty α

Tactic:
obtain ⟨p, _⟩ := (SetRel.finiteDimensional_iff _).mp ‹_›

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
p : RelSeries {(a, b) | a < b}
h✝ : ∀ (y : RelSeries {(a, b) | a < b}), y.length ≤ p.length
⊢ Nonempty α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
p : LTSeries αᵒᵈ
hp : RelSeries.last p = a
hl : p.length = n
⊢ ∃ p, RelSeries.head p = a ∧ p.length = n

Tactic:
exact ⟨p.reverse, by simpa, by simpa⟩

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
n : N
hn : ∃ b, n + b = 0
m : M
b : N
eq : n + b = 0
⊢ m ⊗ₜ[R] n + m ⊗ₜ[R] b = 0

Tactic:
by rw [← tmul_add, eq, tmul_zero]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : i = 0
⊢ (if ⟨i, hi⟩.castSucc = 0 then a else ↑(f ↑⟨i, hi⟩.castSucc), if ⟨i, hi⟩.succ = 0 then a else ↑(f ↑⟨i, hi⟩.succ)) ∈
    {(a, b) | a < b}

Tactic:
subst i
      exact (f 1).prop

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : Multiset ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
⊢ (Multiset.map g t).prod ∈ (Multiset.map f t).prod

Tactic:
induction t using Quotient.inductionOn

Goal state after:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ i ∈ ⟦a✝⟧, g i ∈ f i
⊢ (Multiset.map g ⟦a✝⟧).prod ∈ (Multiset.map f ⟦a✝⟧).prod
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : Multiset ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
⊢ (Multiset.map f₁ t).prod ⊆ (Multiset.map f₂ t).prod

Tactic:
induction t using Quotient.inductionOn

Goal state after:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ i ∈ ⟦a✝⟧, f₁ i ⊆ f₂ i
⊢ (Multiset.map f₁ ⟦a✝⟧).prod ⊆ (Multiset.map f₂ ⟦a✝⟧).prod
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ a * 1 ↔ x ∈ a

Tactic:
simp only [mem_mul, mem_one, mul_smul_comm, exists_exists_eq_and, mul_one]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ y ∈ a, ∃ a, a • y = x) ↔ x ∈ a
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
P Q : Submodule R A
x : A
hx : x ∈ span R ↑P * span R ↑Q
⊢ x ∈ span R (↑P * ↑Q)

Tactic:
Submodule.span_mul_span

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
P Q : Submodule R A
x : A
hx : x ∈ span R (↑P * ↑Q)
⊢ x ∈ span R (↑P * ↑Q)
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case inl.e_I
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ map (RingHom.fst R S) (span (s ×ˢ t)) = span s

Tactic:
rw [Ideal.map_span]
      simp [Set.fst_image_prod _ ht]

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
⊢ map f I ≤ comap g I

Tactic:
refine Ideal.span_le.2 ?_
  rintro x ⟨x, hx, rfl⟩
  rw [SetLike.mem_coe, mem_comap, hf hx]
  exact hx

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
a b : K
⊢ EuclideanDomain.gcd a b = if a = 0 then b else a

Tactic:
by
  unfold EuclideanDomain.gcd
  split_ifs <;> simp [*, Field.mod_eq]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
| comap f (I • map f (comap f p))

Tactic:
← Submodule.map_smul''

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
| comap f (map f (I • comap f p))
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ comap f (map f p) = p ↔ ∃ q, q.IsPrime ∧ comap f q = p

Tactic:
refine ⟨fun hp ↦ ?_, ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
hp : comap f (map f p) = p
⊢ ∃ q, q.IsPrime ∧ comap f q = p

case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ (∃ q, q.IsPrime ∧ comap f q = p) → comap f (map f p) = p
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
obtain rfl | h := eq_or_ne n 0

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m : ℕ
⊢ I ^ (m + 0) = I ^ m * I ^ 0

case inr
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
h : n ≠ 0
⊢ I ^ (m + n) = I ^ m * I ^ n
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c

Tactic:
simp [hc]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

pp: case neg
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

Tactic:
· rw [insert_eq_of_mem h,
      (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]

Goal state after:
case neg
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ Associated 1 a

Tactic:
apply (associated_one_iff_isUnit.mpr hab).symm.trans

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ Associated (gcd a b) a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * (b' * a')) = d₂ ^ k * (b' * (d₁ ^ k * a'))

Tactic:
← mul_assoc _ b',

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * (d₁ ^ k * a'))
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
h' : a' * b' = 1
⊢ Associated (d₁ ^ k) a

Tactic:
use Units.mkOfMulEqOne _ _ h'

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
h' : a' * b' = 1
⊢ d₁ ^ k * ↑(Units.mkOfMulEqOne a' b' h') = a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (I ^ (n + 2)).radical = I.radical

Tactic:
rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ⇑f
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
by
  let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
  let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
  exact le_of_fin_surjective R
    (Q.symm.toLinearMap ∘ₗ f ∘ₗ P) (Q.symm.surjective.comp (i.comp P.surjective))

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : RankCondition R
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Surjective ⇑f
g : M →ₗ[R] Fin (n + 1) → R
hg : Surjective ⇑g
⊢ False

Tactic:
by simpa using le_of_fin_surjective R (g ∘ₗ f) (hg.comp hf)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
⊢ a ∣ Classical.choose ⋯

Tactic:
have h0 : lcm c b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹c = 0› h
        · exact absurd ‹b = 0› h_1

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
⊢ a ∣ Classical.choose ⋯
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : IsEmpty n
M N : Matrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
exact isEmptyElim j

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
by
  have : Finite ι := i.finite_of_le_span_finite v w s
  let := Fintype.ofFinite ι
  rw [Cardinal.mk_fintype]
  simp only [Nat.cast_le]
  exact linearIndependent_le_span_aux' v i w s

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case pos
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : a j = 0
⊢ Pi.single j 1 ≠ 0 ∧ Pi.single j 1 ⬝ᵥ a = 0

pp: case neg
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : ¬a j = 0
⊢ (fun k ↦ if k = i then a j else if k = j then -a i else 0) ≠ 0 ∧
    (fun k ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0

Tactic:
· simp [h2]

Goal state after:
case neg
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : ¬a j = 0
⊢ (fun k ↦ if k = i then a j else if k = j then -a i else 0) ≠ 0 ∧
    (fun k ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i i' : m
hi : i ≠ i'
j j' : n
a : α
⊢ single i j a i' j' = 0

Tactic:
simp [hi]

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

Goal state before:
pp: case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∉ s
i : ι
his : i ∈ s
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s :=
          ⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩

Goal state after:
case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
⊢ ∃ y, ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
obtain ⟨y, i, hmem, hi⟩ := Ideal.IsMaximal.exists_inv ‹_› hx

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ ∃ y, ∃ i ∈ I ^ n, y * x + i = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ (finsuppTotal ι M I v) f = f.sum fun i x ↦ ↑x • v i

Tactic:
by
  dsimp [finsuppTotal]
  rw [Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]
  exact fun _ => zero_smul _ _

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ((b.smulTower c).repr (b (i, j).1 • c (i, j).2)) (i', j') = (single (i, j) 1) (i', j')

Tactic:
rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ (b.repr (b (i, j).1 • if (i, j).2 = (i', j').2 then 1 else 0)) (i', j').1 = (single (i, j) 1) (i', j')
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ (b.repr (b i • 0)) i' = (single (i, j) 1) (i', j')

Tactic:
simp [hi]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = s.card • {a}

Tactic:
refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩
  · rw [card_eq_zero.1 h, toFinset_zero] at H
    exact Finset.empty_ne_singleton _ H
  · rw [count_nsmul, count_singleton]
    by_cases hx : x = a
    · simp_rw [hx, ite_true, mul_one, count_eq_card]
      intro y hy
      rw [← mem_toFinset, H, Finset.mem_singleton] at hy
      exact hy.symm
    have hx' : x ∉ s := fun h' ↦ hx <| by rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
    simp_rw [count_eq_zero_of_notMem hx', hx, ite_false, Nat.mul_zero]
  simpa only [toFinset_nsmul _ _ H.1, toFinset_singleton] using congr($(H.2).toFinset)

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

Goal state before:
pp: case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)

pp: case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
· obtain ⟨b, hb⟩ := exists_ne (0 : β)
      exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩

Goal state after:
case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: case neg
n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : ¬i = j
⊢ 0 ≤ 1 i j

Tactic:
simp [hi]

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ fromAddMonoid ((of (fun i ↦ γ →+ β i) i) f) = (of β i).comp f

Tactic:
fromAddMonoid,

Goal state after:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ (toAddMonoid fun i ↦ AddMonoidHom.compHom (of β i)) ((of (fun i ↦ γ →+ β i) i) f) = (of β i).comp f
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst✝² : SMul X R
inst✝¹ : SMul X A
inst✝ : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ ↑(((x • 1) • s) • t) = ↑(x • (1 • s) • t)

Tactic:
one_smul,

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst✝² : SMul X R
inst✝¹ : SMul X A
inst✝ : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ ↑(((x • 1) • s) • t) = ↑(x • s • t)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ S → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ S ≤ S ⊔ T
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ T → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ T ≤ S ⊔ T