mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.DedekindZeta

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 < dedekindZeta_residue K

Tactic:
by
  refine div_pos ?_ ?_
  · exact mul_pos (mul_pos (by positivity) (regulator_pos K)) (Nat.cast_pos.mpr (classNumber_pos K))
  · exact mul_pos (Nat.cast_pos.mpr (torsionOrder_pos K)) <|
      Real.sqrt_pos_of_pos <| abs_pos.mpr (Int.cast_ne_zero.mpr (discr_ne_zero K))

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
hα : IsIntegral ℤ α
hα0 : α ≠ 0
σ : K →+* ℂ
hσ : 1 ≤ ‖σ α‖
⊢ 1 ≤ house α

Tactic:
apply hσ.trans (norm_embedding_le_house α σ)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖σ' α * ∏ τ ∈ univ.erase σ', τ α‖ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖

Tactic:
rw [Complex.norm_mul]

Goal state after:
case calc_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖σ' α‖ * ‖∏ τ ∈ univ.erase σ', τ α‖ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
hmulvec0 : ∑ y, ∑ x_1, a' K a k x_1 y u * x (x_1, y) = 0 (k, u)
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0

Tactic:
exact mod_cast hmulvec0

Goal state after:
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun x ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
⊢ ‖f x‖ ≤ ‖↑k.factorial‖

Tactic:
have hC : (k.factorial : ℤ_[p]) ≠ 0 := Nat.cast_ne_zero.mpr k.factorial_ne_zero

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun x ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
⊢ ‖f x‖ ≤ ‖↑k.factorial‖
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-↑n)
H : ¬x' - y' = 0
⊢ (↑p ^ padicValRat p (x' - y'))⁻¹ ≤ (↑p ^ n)⁻¹

Tactic:
· simp only [H, ↓reduceIte, exp_lt_exp, neg_lt_neg_iff] at h
        simpa [hp0', zpow_pos, pow_pos, inv_le_inv₀] using
          zpow_right_mono₀ (by exact_mod_cast (Nat.Prime.one_le Fact.out)) h.le

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case ofNat.zero
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
⊢ (a ^ Int.ofNat 0).y.sign = (Int.ofNat 0).sign

pp: case ofNat.succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.ofNat (n + 1)).y.sign = (Int.ofNat (n + 1)).sign

pp: case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign

Tactic:
· rfl

Goal state after:
case ofNat.succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.ofNat (n + 1)).y.sign = (Int.ofNat (n + 1)).sign

case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (-a₁ ^ n₂).x
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁

Tactic:
rw [x_neg, lt_neg] at Hx

Goal state after:
case inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : (a₁ ^ n₂).x < -1
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg.a.a.h
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ d1.lcm d2 ∈ n.divisors

Tactic:
rw [mem_divisors, Nat.lcm_dvd_iff]

Goal state after:
case neg.a.a.h
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ (d1 ∣ n ∧ d2 ∣ n) ∧ n ≠ 0
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0
x : ℤ
hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y
⊢ x + (((f (σ 2) - f (σ 3)) / 2) ^ 2 + ((f (σ 2) + f (σ 3)) / 2) ^ 2) = m

Tactic:
← Int.sq_add_sq_of_two_mul_sq_add_sq hy.symm,

Goal state after:
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0
x : ℤ
hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y
⊢ x + y = m
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b :
  (Submodule.mkQ (map f p)) x ∈ Submodule.map (↑R (Submodule.mkQ (map f p))) (Submodule.span R (Set.range b'))
y : S
y_mem : y ∈ Submodule.span R (Set.range b')
y_eq : (↑R (Submodule.mkQ (map f p))) y = (Submodule.mkQ (map f p)) x
⊢ y + -(y - x) ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map f p)

Tactic:
LinearMap.restrictScalars_apply,

Goal state after:
case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b :
  (Submodule.mkQ (map f p)) x ∈ Submodule.map (↑R (Submodule.mkQ (map f p))) (Submodule.span R (Set.range b'))
y : S
y_mem : y ∈ Submodule.span R (Set.range b')
y_eq : (Submodule.mkQ (map f p)) y = (Submodule.mkQ (map f p)) x
⊢ y + -(y - x) ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map f p)
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ¬_root_.Prime ↑p

Tactic:
prime_iff_mod_four_eq_three_of_nat_prime p

Goal state after:
p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ¬p % 4 = 3
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.left
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
⊢ ¬↑p ∣ eval 0 f ^ p + ↑p * eval 0 gp'

Tactic:
rw [dvd_add_left (dvd_mul_right _ _)]
    contrapose! p_gt with h
    exact Nat.le_of_dvd (Int.natAbs_pos.mpr hf) (Int.natCast_dvd.mp (Int.Prime.dvd_pow' prime_p h))

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
hy : eval (↑z / ↑↑(a + 1)) (map (algebraMap ℤ ℝ) f) = 0
⊢ ↑z / ↑(↑a + 1) ∈ {α}

Tactic:
refine U.subset ?_

Goal state after:
case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
hy : eval (↑z / ↑↑(a + 1)) (map (algebraMap ℤ ℝ) f) = 0
⊢ ↑z / ↑(↑a + 1) ∈ closedBall α ζ ∩ ↑fR.roots.toFinset
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
⊢ 1 < ↑b

Tactic:
rw [← Int.cast_one]; exact Int.cast_lt.mpr b1

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case neg
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)
hPe : ¬FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
simp only [finrank_of_infinite_dimensional hP, finrank_of_infinite_dimensional hPe,
    mul_zero]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: ⊢ {x | Liouville x} ∈ residual ℝ

Tactic:
setOfPred_liouville_eq_irrational_inter_iInter_iUnion

Goal state after:
⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ∈ residual ℝ
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |↑r| * (C / ↑n ^ p) = ↑|r| * (C / ↑n ^ p)

Tactic:
simp only [Rat.cast_abs]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 1 / (↑n + 1) < p - 2
⊢ x ∈
    ⋃ m,
      (fun x ↦ x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

Tactic:
rw [lt_sub_iff_add_lt'] at hn

Goal state after:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
⊢ x ∈
    ⋃ m,
      (fun x ↦ x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
lowerPolar_intent✝¹ : lowerPolar r (upperPolar r s₁) = s₁
s₂ : Set α
lowerPolar_intent✝ : lowerPolar r (upperPolar r s₂) = s₂
h :
  { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝¹ }.extent =
    { extent := s₂, intent := upperPolar r s₂, upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝ }.extent
⊢ { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝¹ } =
    { extent := s₂, intent := upperPolar r s₂, upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝ }

Tactic:
subst h

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
lowerPolar_intent✝¹ : lowerPolar r (upperPolar r s₁) = s₁
lowerPolar_intent✝ :
  lowerPolar r
      (upperPolar r
        { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯,
            lowerPolar_intent := lowerPolar_intent✝¹ }.extent) =
    { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝¹ }.extent
⊢ { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝¹ } =
    {
      extent :=
        { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯,
            lowerPolar_intent := lowerPolar_intent✝¹ }.extent,
      intent :=
        upperPolar r
          { extent := s₁, intent := upperPolar r s₁, upperPolar_extent := ⋯,
              lowerPolar_intent := lowerPolar_intent✝¹ }.extent,
      upperPolar_extent := ⋯, lowerPolar_intent := lowerPolar_intent✝ }
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t₁ : Set β
upperPolar_extent✝¹ : upperPolar r (lowerPolar r t₁) = t₁
t₂ : Set β
upperPolar_extent✝ : upperPolar r (lowerPolar r t₂) = t₂
h :
  { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹, lowerPolar_intent := ⋯ }.intent =
    { extent := lowerPolar r t₂, intent := t₂, upperPolar_extent := upperPolar_extent✝, lowerPolar_intent := ⋯ }.intent
⊢ { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹, lowerPolar_intent := ⋯ } =
    { extent := lowerPolar r t₂, intent := t₂, upperPolar_extent := upperPolar_extent✝, lowerPolar_intent := ⋯ }

Tactic:
subst h

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
t₁ : Set β
upperPolar_extent✝¹ : upperPolar r (lowerPolar r t₁) = t₁
upperPolar_extent✝ :
  upperPolar r
      (lowerPolar r
        { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹,
            lowerPolar_intent := ⋯ }.intent) =
    { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹, lowerPolar_intent := ⋯ }.intent
⊢ { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹, lowerPolar_intent := ⋯ } =
    {
      extent :=
        lowerPolar r
          { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹,
              lowerPolar_intent := ⋯ }.intent,
      intent :=
        { extent := lowerPolar r t₁, intent := t₁, upperPolar_extent := upperPolar_extent✝¹,
            lowerPolar_intent := ⋯ }.intent,
      upperPolar_extent := upperPolar_extent✝, lowerPolar_intent := ⋯ }
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
⊢ (rcomap r (rcomap s l)).sets = (rcomap (r.comp s) l).sets

Tactic:
by
    ext t
    simp only [rcomap_sets, SetRel.image, Filter.mem_sets, Set.mem_ofPred_eq, SetRel.core_comp]
    constructor
    · rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
      exact ⟨v, vsets, Set.Subset.trans (SetRel.core_mono hv) h⟩
    rintro ⟨t, tsets, ht⟩
    exact ⟨SetRel.core s t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩

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

Goal state before:
pp: α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂

Tactic:
rtendsto_def

Goal state after:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
hs : s ∈ cardinalGenerate g hc
⊢ s ∈ f

Tactic:
induction hs with

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : StrictMono f
x : α
hx : x < f 0
⊢ StrictMono (insertNth 0 x f)

Tactic:
Fin.strictMono_iff_lt_succ

Goal state after:
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
x : α
hx : x < f 0
⊢ ∀ (i : Fin (n + 1)), insertNth 0 x f i.castSucc < insertNth 0 x f i.succ
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : StrictMono f
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ StrictMono (i.castSucc.succ.insertNth x f)

Tactic:
Fin.strictMono_iff_lt_succ

Goal state after:
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ ∀ (i_1 : Fin (n + 1)), i.castSucc.succ.insertNth x f i_1.castSucc < i.castSucc.succ.insertNth x f i_1.succ
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LE α
⊢ (univ.chainHeight fun x1 x2 ↦ x1 ≤ x2) = s.chainHeight fun x1 x2 ↦ x1 ≤ x2

Tactic:
by
  simpa using chainHeight_coe_univ s (· ≤ ·)

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : StrictMono f
x : α
hx : f (last n) < x
⊢ StrictMono ((last (n + 1)).insertNth x f)

Tactic:
Fin.strictMono_iff_lt_succ

Goal state after:
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
x : α
hx : f (last n) < x
⊢ ∀ (i : Fin (n + 1)), (last (n + 1)).insertNth x f i.castSucc < (last (n + 1)).insertNth x f i.succ
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
hb : (Ici b).Infinite
h : ∀ (a : { a // (Ici a).Infinite }), ∃ b, ↑a ⋖ b ∧ (Ici b).Infinite :=
  fun a ↦ exists_covby_infinite_Ici_of_infinite_Ici a.property (hfin ↑a)
ks : ℕ → { a // (Ici a).Infinite } := fun t ↦ Nat.rec ⟨b, hb⟩ (fun x a ↦ ⟨⋯.choose, ⋯⟩) t
i : ℕ
⊢ (fun i ↦ ↑(ks i)) i ⋖ (fun i ↦ ↑(ks i)) (i + 1)

Tactic:
simpa using (h (ks i)).choose_spec.1

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
⊢ ∀ {w x y z : α}, r w x → r y z → r (w ⊓ y) (x ⊓ z)

Tactic:
intro w _ _ _ h1 h2
    have compatible_left_inf {x y t : α} (hh : r x y) : r (x ⊓ t) (y ⊓ t) :=
      closed_interval h₂ h₄ ((x ⊓ y) ⊓ t) _ _ ((x ⊔ y) ⊓ t)
            (inf_le_inf_right _ inf_le_left) (inf_le_inf_right _ le_sup_left)
            (inf_le_inf_right _ inf_le_right) (inf_le_inf_right _ le_sup_right)
            (h₄ inf_le_sup (h₂.mp hh)).1
    exact transitive h₂ h₃ h₄ (by
          simpa [inf_comm w] using compatible_left_inf h2) (compatible_left_inf h1)

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
⊢ y ∈ I

Tactic:
have hyJ : y ∈ (J : Set P) := Set.eq_univ_iff_forall.mp hJuniv y

Goal state after:
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
hyJ : y ∈ ↑J
⊢ y ∈ I
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : I.IsPrime
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : y ∉ ↑I
⊢ x ∈ ↑J

Tactic:
suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J by rwa [sup_inf_inf_compl] at ass

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : I.IsPrime
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : y ∉ ↑I
⊢ x ⊓ y ⊔ x ⊓ yᶜ ∈ J
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case refine_1.a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨆ y ∈ Y, f a y ≤ f a b

Tactic:
simp only [iSup_le_iff]
      exact h a ha

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_2.inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
h : a ≠ a → P.Rel a a
⊢ f a = f a

pp: case refine_2.inr
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h : a ≠ b → P.Rel a b
hne : a ≠ b
⊢ f a = f b

Tactic:
· rfl

Goal state after:
case refine_2.inr
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h : a ≠ b → P.Rel a b
hne : a ≠ b
⊢ f a = f b
Module: Mathlib.Order.Std

Goal state before:
pp: case isTrue.isFalse
α : Type u_1
args : OfStdArgs α
this✝⁵ : LE α := args.le
this✝⁴ : LT α := args.lt
this✝³ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝² :
  let this := args.le;
  Std.IsLinearOrder α
this✝¹ : DecidableLE α := args.decidableLE
this✝ : Std.LawfulOrderLeftLeaningMin α
this : Std.LawfulOrderLeftLeaningMax α
a b : α
h✝¹ : b ≤ a
h✝ : ¬a ≤ b
⊢ a = a

Tactic:
· rfl

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case pos
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = f₀ h₂.choose

Tactic:
exact h₁ ⟨_, hab.trans h₂.choose_spec⟩ |>.elim

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

Goal state before:
pp: t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
a : ↑t
h : a = ⊥
ha : a ∈ ↑t₁
hb : a ∈ ↑t₂
⊢ False

Tactic:
subst h

Goal state after:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
ha : ⊥ ∈ ↑t₁
hb : ⊥ ∈ ↑t₂
⊢ False
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a b : X
S : Sublocale X
s : Set X
⊢ Sublocale.restrictAux✝ S (sSup s) = sSup ((fun x ↦ sInf {s | x ≤ ↑s}) '' s)

Tactic:
rw [S.giAux.gc.l_sSup, sSup_image]

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a b : X
S : Sublocale X
s : Set X
⊢ ⨆ a ∈ s, Sublocale.restrictAux✝ S a = ⨆ a ∈ s, sInf {s | a ≤ ↑s}