mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (A.submatrix ⇑e₁ ⇑e₂) := A.submatrixEquivInvertible e₁ e₂
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁

Tactic:
invOf_submatrix_equiv_eq A

Goal state after:
case pos.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (A.submatrix ⇑e₁ ⇑e₂) := A.submatrixEquivInvertible e₁ e₂
⊢ (⅟A).submatrix ⇑e₂ ⇑e₁ = (⅟A).submatrix ⇑e₂ ⇑e₁
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹) = kroneckerMap (fun x1 x2 ↦ x1 * x2) 1 1

Tactic:
mul_nonsing_inv _ hA,

Goal state after:
case pos
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) 1 (B * B⁻¹) = kroneckerMap (fun x1 x2 ↦ x1 * x2) 1 1
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case e_m
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
i' j✝ : n
⊢ (x • single i j 1) i' j✝ =
    ((LinearMap.mul R (Matrix n n R)) (single i j x, 1).1, (LinearMap.mul R R[X]) (single i j x, 1).2).1 (1, X ^ k).1 i'
      j✝

Tactic:
simp [single]

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case e_n
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
i' : ℕ
⊢ (X ^ k).coeff i' =
    (((LinearMap.mul R (Matrix n n R)) (single i j x, 1).1, (LinearMap.mul R R[X]) (single i j x, 1).2).2
          (1, X ^ k).2).coeff
      i'

Tactic:
simp [single]

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : (matPolyEquiv m).coeff k = 0
⊢ (m i j).coeff k = 0

Tactic:
rw [← matPolyEquiv_coeff_apply, hk, Matrix.zero_apply]

Goal state after:
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + b
⊢ a' = b'

Tactic:
exact add_right_cancel H

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent ((reflect N P).coeff i)

pp: case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
· simpa [hi, revAt_le] using h (N - i)

Goal state after:
case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent ((reflect N P).coeff i)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : (f P).degree = 0 ∧ (f Q).degree = 0
hcoeff : P.coeff n ∈ I
⊢ P.coeff n ∈ I

Tactic:
exact hcoeff

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
H : Function.Surjective ⇑(algebraMap R S)
N : Submodule S M
⊢ (restrictScalars R N).spanRank ≤ N.spanRank

Tactic:
obtain ⟨s, hs, rfl⟩ := N.exists_span_set_card_eq_spanRank

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
H : Function.Surjective ⇑(algebraMap R S)
s : Set M
hs : Cardinal.mk ↑s = (span S s).spanRank
⊢ (restrictScalars R (span S s)).spanRank ≤ (span S s).spanRank
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
hx : IsIntegral R x
⊢ (Subalgebra.toSubmodule R[x]).FG

Tactic:
rcases hx with ⟨f, hfm, hfx⟩
  use (Finset.range <| f.natDegree).image (x ^ ·)
  exact span_range_natDegree_eq_adjoin hfm (by rwa [aeval_def])

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
⊢ IsIntegral R a

Tactic:
have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by
      have : RingHomInvPair (φ : R →+* T) φ.symm := RingHomInvPair.of_ringEquiv _
      simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]
    let : Algebra T R := φ.symm.toRingHom.toAlgebra
    let : IsScalarTower T R S :=
      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl⟩
    exact IsIntegral.tower_top ha

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det = 1 + M.trace • X + (1 + X • M.map ⇑C).det.divX.divX * X ^ 2

Tactic:
rw [Algebra.smul_def (trace M), ← C_eq_algebraMap, pow_two, ← mul_assoc, add_assoc,
    ← add_mul, ← coeff_det_one_add_X_smul_one, ← coeff_divX, add_comm (C _), divX_mul_X_add,
    add_comm (1 : R[X]), ← C.map_one]
  convert! (divX_mul_X_add _).symm
  rw [coeff_zero_eq_eval_zero, eval_det_add_X_smul, det_one, eval_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ ∑ x, 1 = Fintype.card n

Tactic:
Finset.sum_const,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ #univ • 1 = Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
⊢ p - 1 = X * (p /ₘ X)

Tactic:
conv_lhs => rw [← modByMonic_add_div p X]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
⊢ p %ₘ X + X * (p /ₘ X) - 1 = X * (p /ₘ X)
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
a✝ : Nontrivial R
n : ℕ
c : R
⊢ c ≠ 0 → ((taylor r) ((monomial n) c)).natDegree = n

Tactic:
c0

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
a✝ : Nontrivial R
n : ℕ
c : R
c0 : c ≠ 0
⊢ ((taylor r) ((monomial n) c)).natDegree = n
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
n : ℕ
⊢ n ∈ Finset.range (p.natDegree + 1) →
    f (p.integralNormalization.coeff n) * (f p.leadingCoeff * x) ^ n =
      f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff n) * x ^ n)

Tactic:
_hn

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
n : ℕ
_hn : n ∈ Finset.range (p.natDegree + 1)
⊢ f (p.integralNormalization.coeff n) * (f p.leadingCoeff * x) ^ n =
    f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff n) * x ^ n)
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr.cons.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH : ((Multiset.map (fun x ↦ X + C x) s).prod.scaleRoots r).Splits
⊢ (X + C a).leadingCoeff * (Multiset.map (fun x ↦ X + C x) s).prod.leadingCoeff ≠ 0

Tactic:
· simp only [leadingCoeff_X_add_C, one_mul, ne_eq, leadingCoeff_eq_zero]
        exact (monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).ne_zero

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
a✝ : Nontrivial R
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
a : R
ha : a ∈ m
⊢ f.natDegree ≤ 1

Tactic:
· obtain ⟨m, rfl⟩ := Multiset.exists_cons_of_mem ha
    rw [Multiset.map_cons, Multiset.prod_cons] at hm
    rw [hm] at h
    simp only [irreducible_mul_iff, IsUnit.mul_iff, not_isUnit_X_add_C, false_and, and_false,
      or_false, false_or, ← Multiset.prod_toList, List.prod_isUnit_iff] at h
    have : m = 0 := by simpa [not_isUnit_X_add_C, ← Multiset.eq_zero_iff_forall_notMem] using h.1.2
    grw [hm, this, natDegree_mul_le]
    simp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
h'' : p = 0
⊢ False

Tactic:
h'',

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ natDegree 0
h'' : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (f * g).natDegree + 1 = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ ((X - C a) * f).Splits ∧ g.Splits

Tactic:
Nat.succ_inj

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a ((X - C a) * (f * g)) = 0
⊢ ((X - C a) * f).Splits ∧ g.Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegralClosure A R B
A' : Type u_4
inst✝⁶ : CommRing A'
inst✝⁵ : Algebra A' B
inst✝⁴ : IsIntegralClosure A' R B
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R A' B
x : A
⊢ ((lift R A B).comp (lift R A' B)) x = (AlgHom.id R A) x

Tactic:
apply algebraMap_injective A R B

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegralClosure A R B
A' : Type u_4
inst✝⁶ : CommRing A'
inst✝⁵ : Algebra A' B
inst✝⁴ : IsIntegralClosure A' R B
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R A' B
x : A
⊢ (algebraMap A B) (((lift R A B).comp (lift R A' B)) x) = (algebraMap A B) ((AlgHom.id R A) x)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left✝¹ : m'.IsMaximal
left✝ : (comap (algebraMap R S) m').IsMaximal
hm : I ≤ comap (algebraMap R S) m'
⊢ ¬map f I = ⊤

Tactic:
← map_le_iff_le_comap

Goal state after:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left✝¹ : m'.IsMaximal
left✝ : (comap (algebraMap R S) m').IsMaximal
hm : map (algebraMap R S) I ≤ m'
⊢ ¬map f I = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ I ∉ zeroLocus {f} ↔ f ∉ I.asIdeal

Tactic:
mem_zeroLocus,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ ¬{f} ⊆ ↑I.asIdeal ↔ f ∉ I.asIdeal
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsAlgebraic R (a + b)

Tactic:
refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero b0 a0, ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R ((rb * ra) • (a + b))
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : Function.Surjective ⇑f
x✝¹ : Ideal S
x✝ : x✝¹ ≠ ⊤
s : S
r : R
hr : f r = s
⊢ 1 * f 1 * s = 1 * f r

Tactic:
simp [hr]

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
⊢ (r₁ • r₂) • t₁ • t₂ = (r₁ • t₁) • r₂ • t₂

Tactic:
rw [smul_smul_smul_comm]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
x : R
⊢ (algebraMap R I.ResidueField) x = 0 ↔ x ∈ I

Tactic:
rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I),
    IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff]
  exact IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : FaithfullyFlat A B
a₁ a₂ : A
ha : ∀ (a : B), a₁ • a = a₂ • a
⊢ 1 ⊗ₜ[A] (a₁ * 1) = 1 ⊗ₜ[A] (a₂ * 1)

Tactic:
simp only [← smul_eq_mul, ← TensorProduct.smul_tmul, ha (1 : B)]

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
U : Opens α
⊢ IsOpen[inst✝¹] ↑U

Tactic:
exact U.2

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mpr.refine_1
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
U : Opens α
⊢ IsOpen[inst✝] ↑U

Tactic:
exact U.2

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
V : Set α
hV : IsOpen[inst✝¹] V
⊢ f '' V = ⋃ i, f '' Subtype.val '' Subtype.val ⁻¹' V

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
V : Set α
hV : IsOpen[inst✝¹] V
⊢ f '' V = ⋃ i, f '' (V ∩ range Subtype.val)
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = sSup S₁ ⊔ sSup S₂

Tactic:
← h₁,

Goal state after:
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = s ⊓ z₁ ⊔ sSup S₂
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2) =
    ({(z, ⟨↑x ⊔ ↑w, ⋯⟩), (⟨↑y ⊓ ↑z, ⋯⟩, w)} ∪ t).sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
simp_rw [Finset.sup_union, Finset.sup_insert, Finset.sup_singleton, _root_.sdiff_eq,
    compl_sup, inf_left_comm z.1, compl_inf, compl_compl, inf_sup_right, inf_assoc]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f '' f ⁻¹' (U ∩ V) = U ∩ V

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ U ∩ V ∩ range f = U ∩ V
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f '' f ⁻¹' U = U

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ U ∩ range f = U
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f '' f ⁻¹' V = V

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ V ∩ range f = V
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
⊢ Function.Injective (Compacts.map f hf) ↔ Function.Injective f

Tactic:
by
  refine ⟨fun h => .of_comp (f := ({·} : β → Compacts β)) ?_, map_injective hf⟩
  simp_rw [Function.comp_def, ← map_singleton hf]
  exact h.comp singleton_injective

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed[inst✝²] S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ f '' closure[inst✝²] {y} = f '' S✝

Tactic:
rw [← hx.def, ← hf.closure_image_eq, image_singleton]

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
⊢ IsConstructible ((U ∩ V) ↓∩ (s ∪ t))

Tactic:
have : (U ∩ V) ↓∩ (s ∪ t) =
      inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∪ inclusion inter_subset_right ⁻¹' (V ↓∩ t) := by
    ext; simp

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
this : (U ∩ V) ↓∩ (s ∪ t) = inclusion ⋯ ⁻¹' U ↓∩ s ∪ inclusion ⋯ ⁻¹' V ↓∩ t
⊢ IsConstructible ((U ∩ V) ↓∩ (s ∪ t))
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), f 1 * x = f x
g : AddAut (ZMod n)
⊢ (fun x ↦ AddAut.mulLeft (Additive.toMul x)) ((fun f ↦ Additive.ofMul (Units.mkOfMulEqOne (f 1) ((-f) 1) ⋯)) g) = g

Tactic:
simp [DFunLike.ext_iff, Units.smul_def, h]

Goal state after: