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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocCommSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
⊢ (mul R A).flip = mul R A

Tactic:
by ext; simp [mul_comm]

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
α : Type u_22
s : Finset α
n : α → N
⊢ m ⊗ₜ[R] ∑ a ∈ s, n a = ∑ a ∈ s, m ⊗ₜ[R] n a

Tactic:
by
  classical
    induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, tmul_add, ih]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass R R ↥x
c : R →₀ ↥x
hc1 : ↑c.support ⊆ t
hm : ↑(c.sum fun r m ↦ r • m) ∈ t • x
⊢ r • ∑ i ∈ c.support, ↑(i • c i) ∈ (s * t) • x

Tactic:
simp only [SetLike.val_smul, Finset.smul_sum, smul_smul]

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass R R ↥x
c : R →₀ ↥x
hc1 : ↑c.support ⊆ t
hm : ↑(c.sum fun r m ↦ r • m) ∈ t • x
⊢ ∑ x_1 ∈ c.support, (r * x_1) • ↑(c x_1) ∈ (s * t) • x
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_9
Q : Type u_10
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R P
inst✝ : Module R Q
p p' : Submodule R P
q q' : Submodule R Q
hp : p ≤ p'
hq : q ≤ q'
⊢ p.subtype.range ≤ p'.subtype.range

Tactic:
by simpa

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_9
Q : Type u_10
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R P
inst✝ : Module R Q
p p' : Submodule R P
q q' : Submodule R Q
hp : p ≤ p'
hq : q ≤ q'
⊢ q.subtype.range ≤ q'.subtype.range

Tactic:
by simpa

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hj.choose < ↑hi.choose
⊢ hj.choose < hi.choose

Tactic:
by simpa

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ ¬toInt val i ≤ toInt val j ↔ ¬val i ≤ val j

Tactic:
by
  simpa using toInt_lt_toInt val j i

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

Goal state before:
pp: case cons.mp.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
⊢ ∑ i ∈ t, (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x ↦ s a) i * ∏ j ∈ t \ {i}, s j = 1

Tactic:
rw [prod_eq_mul_prod_sdiff_singleton_of_mem h.choose_spec, ← mul_assoc, ←
          @if_pos _ _ h.choose_spec R (_ * _) 0, ← sum_pi_single', ← sum_add_distrib] at hμ
        rw [← hμ, sum_congr rfl]
        intro x hx
        convert! add_mul (R := R) _ _ _ using 2
        · by_cases hx : x = h.choose
          · rw [hx, Pi.single_eq_same, Pi.single_eq_same]
          · rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
        · convert! (mul_assoc _ _ _).symm
          rw [prod_eq_prod_sdiff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
h : x⁻¹ * y ∈ p
⊢ (DistribSMul.toLinearMap R S x) (x⁻¹ * y) = y

Tactic:
by simp [mul_inv_cancel_left₀ hx]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ (I.prod J).IsPrime → I = ⊤ ∨ J = ⊤

Tactic:
contrapose!
  simp only [ne_top_iff_one, isPrime_iff, not_and, not_forall, not_or]
  exact fun ⟨hI, hJ⟩ _ => ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩

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

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
⊢ (comap (Pi.evalRingHom R i) I).IsMaximal

Tactic:
refine isMaximal_iff.mpr ⟨I.ne_top_iff_one.mp h.ne_top, fun J x le hxI hxJ ↦ ?_⟩
  have ⟨r, y, hy, eq⟩ := h.exists_inv hxI
  classical
  convert!
    J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y)
      (le <| by apply update_self i y 1 ▸ hy)
  ext j
  obtain rfl | ne := eq_or_ne j i
  · simpa [eq_comm] using eq
  · simp [update_of_ne ne]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : Semiring T
g : T →+* R
f : R →+* S
hf : Function.Injective ⇑f
⊢ Ideal.comap g (ker f) = ker g

Tactic:
(injective_iff_ker_eq_bot f).mp hf,

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : Semiring T
g : T →+* R
f : R →+* S
hf : Function.Injective ⇑f
⊢ Ideal.comap g ⊥ = ker g
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : ∀ (m : M'), x • m = 0
m : M
⊢ f (x • m) = f 0

Tactic:
map_smul,

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : ∀ (m : M'), x • m = 0
m : M
⊢ x • f m = f 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ (∀ n ∈ span R s, r • n = 0) → ∀ (n : ↑s), r • ↑n = 0

Tactic:
intro h n
    exact h _ (Submodule.subset_span n.prop)

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

Goal state before:
pp: case mpr.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ x ∈ s, r • x = 0

Tactic:
intro x hx
      exact h ⟨x, hx⟩

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = pmap (fun a h ↦ s.gcd * f h) s ⋯

Tactic:
conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]

Goal state after:
case neg.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ pmap (fun a x ↦ id a) s ⋯ = pmap (fun a h ↦ s.gcd * f h) s ⋯
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ n = ⊤

Tactic:
by
  induction n with
  | zero => simp [J.pow_zero]
  | succ n ih =>
    obtain rfl | hn := eq_or_ne n 0; · simpa [J.pow_one] using h
    rwa [J.pow_succ' hn, sup_mul_eq_of_coprime_right ih]

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

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = pmap (fun a h ↦ s.gcd * f h) s ⋯

Tactic:
conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]

Goal state after:
case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ pmap (fun a x ↦ id a) s ⋯ = pmap (fun a h ↦ s.gcd * f h) s ⋯
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
y : A
mem : y ∈ J
hy : f y = x
⊢ x ∈ map f J

Tactic:
simpa [← hy] using Ideal.mem_map_of_mem _ mem

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
I J : Ideal R
inst✝¹ : I.IsMaximal
inst✝ : J.IsMaximal
ne : I ≠ J
⊢ IsCoprime I J

Tactic:
by
  rw [isCoprime_iff_codisjoint, isMaximal_def] at *
  exact IsCoatom.codisjoint_of_ne ‹_› ‹_› ne

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a b c : α
ha : a ≠ 0
this : gcd (a * b) (a * c) = normalize (a * gcd b c)
⊢ gcd (a * b) (a * c) = normalize a * gcd b c

Tactic:
by simpa

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : gcd (a * b) (a * c) = a * d
⊢ Associated (gcd (a * b) (a * c)) (a * gcd b c)

Tactic:
apply associated_of_dvd_dvd

Goal state after:
case inr.hab
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : gcd (a * b) (a * c) = a * d
⊢ gcd (a * b) (a * c) ∣ a * gcd b c

case hba
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : gcd (a * b) (a * c) = a * d
⊢ a * gcd b c ∣ gcd (a * b) (a * c)
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
trans gcd d₁ b ^ k

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd (d₁ ^ k) b ∣ gcd d₁ b ^ k

α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ^ k ∣ 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a b c : α
ha : a ≠ 0
this : lcm (a * b) (a * c) = normalize (a * lcm b c)
⊢ lcm (a * b) (a * c) = normalize a * lcm b c

Tactic:
by simpa

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : OrzechProperty R
⊢ StrongRankCondition R

Tactic:
refine (strongRankCondition_iff_succ R).2 fun n i hi ↦ ?_
  have h : (0 : Fin (n + 1) → R) = update (0 : Fin (n + 1) → R) (Fin.last n) 1 := by
    apply OrzechProperty.injective_of_surjective_of_injective i (.funLeft ..) hi
      (Fin.castSucc_injective _).surjective_comp_right
    ext; simp
  simpa using congr_fun h (Fin.last n)

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 : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ Classical.choose ⋯ ∣ a

Tactic:
have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 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 : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ Classical.choose ⋯ ∣ a
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 : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ Classical.choose ⋯ ∣ b

Tactic:
have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 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 : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ Classical.choose ⋯ ∣ b
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
inst✝ : Free R M
⊢ Nontrivial M ↔ ¬Module.rank R M = 0

Tactic:
← Module.rank_pos_iff_of_free (R := R),

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
⊢ 0 < Module.rank R M ↔ ¬Module.rank R M = 0
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
x : M
h : Bijective ⇑(LinearMap.toSpanSingleton R M x)
⊢ Module.rank R M = 1

Tactic:
rank_eq_one_iff_finrank_eq_one,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
x : M
h : Bijective ⇑(LinearMap.toSpanSingleton R M x)
⊢ finrank R M = 1
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : StrongRankCondition R
h : Bijective ⇑(algebraMap R S)
⊢ Module.rank R S = 1

Tactic:
rank_eq_one_iff_finrank_eq_one,

Goal state after:
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : StrongRankCondition R
h : Bijective ⇑(algebraMap R S)
⊢ finrank R S = 1
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
inst✝ : Module.Finite R M
N : Submodule R M
⊢ ↑(finrank R ↥N) = Module.rank R ↥N

Tactic:
by
  rw [finrank, Cardinal.cast_toNat_of_lt_aleph0]
  exact lt_of_le_of_lt (Submodule.rank_le N) (rank_lt_aleph0 R M)

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

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
inst✝ : Module.Finite K ↥(span K s)
t : Finset M
hts : ↑t ⊆ s
ht_card : t.card = finrank K ↥(span K s)
ht_span : span K ↑t = span K s
ht_indep : LinearIndepOn K id ↑t
e : Fin (finrank K ↥(span K s)) ≃ ↥t := (Finset.equivFinOfCardEq ht_card).symm
⊢ span K (range (Subtype.val ∘ ⇑e)) = span K s

Tactic:
by simpa

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

Goal state before:
pp: case neg
ι : 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
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
· by_cases hbs : b ∈ s
      · obtain ⟨t, hbt, rfl⟩ : ∃ t, b ∉ t ∧ insert b t = s :=
          ⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f b : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
      rcases s.eq_empty_or_nonempty with rfl | hsne
      · rw [Finset.coe_empty, Set.biUnion_empty] at h
        exact (h I.zero_mem).elim
      · obtain ⟨i, his⟩ := hsne
        obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s :=
          ⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f i : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]

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

Goal state before:
pp: R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : ⋃ i ∈ s, ↑(f i) = ⋃ i ∈ t, ↑(f i)
hmem_union : ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ↑I ⊆ ⋃ i ∈ ↑t, ↑(f i)
⊢ ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
hmem_union,

Goal state after:
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : ⋃ i ∈ s, ↑(f i) = ⋃ i ∈ t, ↑(f i)
hmem_union : ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ↑I ⊆ ⋃ i ∈ ↑t, ↑(f i)
⊢ ↑I ⊆ ⋃ i ∈ ↑t, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
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.repr ((c.repr (b (i, j).1 • c (i, j).2)) (i', j').2)) (i', j').1 = (single (i, j) 1) (i', j')

Tactic:
map_smul,

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 • c.repr (c (i, j).2)) (i', j').2)) (i', j').1 = (single (i, j) 1) (i', j')
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), Commute (single i j 1) M

Tactic:
refine ⟨fun ⟨r, hr⟩ i j => hr ▸ Commute.symm ?_,
    fun hM => mem_range_scalar_iff_commute_single.mpr <| fun i j _ => hM i j⟩

Goal state after:
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝ : M ∈ Set.range ⇑(scalar n)
i j : n
r : α
hr : (scalar n) r = M
⊢ Commute ((scalar n) r) (single i j 1)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : l → o
e₂ : m ≃ o
M : Matrix m n α
⊢ submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id

Tactic:
cases nonempty_fintype o
  let A := M.submatrix e₂.symm id
  have : M = A.submatrix e₂ id := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
  rw [this, submatrix_mul_equiv]
  simp only [A, Matrix.one_mul, submatrix_submatrix, Function.comp_id, submatrix_id_id,
    Equiv.symm_comp_self]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
le_def,

Goal state after:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (∀ {x y : Mᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    c ≤ d
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
le_def,

Goal state after:
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (∀ {x y : Rᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    c ≤ d
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
I✝ : TwoSidedIdeal R
inst✝ : Nontrivial R
I J : RingCon R
h : I ≠ J
⊢ { ringCon := I } ≠ { ringCon := J }

Tactic:
contrapose h; aesop

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
r : R
x : A
hx : ϕ x = ψ x
⊢ ϕ (r • x) = ψ (r • x)

Tactic:
map_smul,

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
r : R
x : A
hx : ϕ x = ψ x
⊢ r • ϕ x = ψ (r • x)