harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem isPrimitiveClassified_of_coprime_of_pos (hc : Int.gcd x y = 1) (hzpos : 0 < z) :
    h.IsPrimitiveClassified

Proof state:
case h
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨ y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

Tactic:
tauto

Result:
no goals

Proof state:
case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h1 : x % 2 = 0 ∧ y % 2 = 1
⊢ h.IsPrimitiveClassified

Tactic:
exact h.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h1.right hzpos

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
⊢ h.IsPrimitiveClassified

Tactic:
rcases h.even_odd_of_coprime hc with h1 | h2

Result:
case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h1 : x % 2 = 0 ∧ y % 2 = 1
⊢ h.IsPrimitiveClassified

case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified

Proof state:
case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified

Tactic:
obtain ⟨m, n, H⟩ := h.symm.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h2.left hzpos

Result:
case inr.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨ y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ h.IsPrimitiveClassified

Proof state:
case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified

Tactic:
rw [Int.gcd_comm] at hc

Result:
case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified

Proof state:
case inr.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨ y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ h.IsPrimitiveClassified

Tactic:
use m, n

Result:
case h
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨ y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem jacobson_bot_of_integral_localization
    {R : Type*} [CommRing R] [IsDomain R] [IsJacobsonRing R]
    (Rₘ Sₘ : Type*) [CommRing Rₘ] [CommRing Sₘ] (φ : R →+* S) (hφ : Function.Injective ↑φ) (x : R)
    (hx : x ≠ 0) [Algebra R Rₘ] [IsLocalization.Away x Rₘ] [Algebra S Sₘ]
    [IsLocalization ((Submonoid.powers x).map φ : Submonoid S) Sₘ]
    (hφ' :
      RingHom.IsIntegral (IsLocalization.map Sₘ φ (Submonoid.powers x).le_comap_map : Rₘ →+* Sₘ)) :
    (⊥ : Ideal S).jacobson = (⊥ : Ideal S)

Proof state:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝⁴ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors S hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝³ : (comap (algebraMap S Sₘ) I).IsPrime
this✝² : (comap φ' I).IsPrime
this✝¹ : ⊥.IsPrime
hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ
f : R ⧸ comap φ (comap (algebraMap S Sₘ) I) →+* S ⧸ comap (algebraMap S Sₘ) I :=
  quotientMap (comap (algebraMap S Sₘ) I) φ ⋯
g : S ⧸ comap (algebraMap S Sₘ) I →+* Sₘ ⧸ I := quotientMap I (algebraMap S Sₘ) ⋯
this✝ : (comap φ' I).IsMaximal
this : (comap (algebraMap R Rₘ) (comap φ' I)).IsMaximal
⊢ (comap (algebraMap S Sₘ) I).IsMaximal

Tactic:
have : ((I.comap (algebraMap S Sₘ)).comap φ).IsMaximal := by
  rwa [comap_comap, hcomm, ← comap_comap] at this

Result:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝⁵ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors S hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝⁴ : (comap (algebraMap S Sₘ) I).IsPrime
this✝³ : (comap φ' I).IsPrime
this✝² : ⊥.IsPrime
hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ
f : R ⧸ comap φ (comap (algebraMap S Sₘ) I) →+* S ⧸ comap (algebraMap S Sₘ) I :=
  quotientMap (comap (algebraMap S Sₘ) I) φ ⋯
g : S ⧸ comap (algebraMap S Sₘ) I →+* Sₘ ⧸ I := quotientMap I (algebraMap S Sₘ) ⋯
this✝¹ : (comap φ' I).IsMaximal
this✝ : (comap (algebraMap R Rₘ) (comap φ' I)).IsMaximal
this : (comap φ (comap (algebraMap S Sₘ) I)).IsMaximal
⊢ (comap (algebraMap S Sₘ) I).IsMaximal
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem ContMDiffWithinAt.mdifferentiableWithinAt (hf : ContMDiffWithinAt I I' n f s x)
    (hn : 1 ≤ n) : MDifferentiableWithinAt I I' f s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
n : WithTop ℕ∞
hf : ContMDiffWithinAt I I' n f s x
hn : 1 ≤ n
h : MDifferentiableWithinAt I I' f (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ (extChartAt I' (f x)).source ∈ 𝓝 (f x)

Tactic:
exact extChartAt_source_mem_nhds (f x)

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem DenseRange.comp {g : Y → Z} {f : α → Y} (hg : DenseRange g) (hf : DenseRange f)
    (cg : Continuous g) : DenseRange (g ∘ f)

Proof state:
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous g
⊢ Dense (g '' range f)

Tactic:
exact hg.dense_image cg hf

Result:
no goals

Proof state:
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous g
⊢ DenseRange (g ∘ f)

Tactic:
rw [DenseRange, range_comp]

Result:
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous g
⊢ Dense (g '' range f)
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_monomial_of_ne_zero (n : ℕ) (a : R) (h : a ≠ 0) : order (monomial R n a) = n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ ((monomial R n) a).order = ↑n

Tactic:
rw [order_monomial, if_neg h]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ ((monomial R n) a).order = ↑n

Tactic:
classical
rw [order_monomial, if_neg h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) (i : Nat)
    (hi : i < (zipWith f as bs).size) :
    (zipWith f as bs)[i] = f (as[i]'(by simp at hi; omega)) (bs[i]'(by simp at hi; omega))

Proof state:
α : Type ?u.533946
β : Type ?u.533949
γ : Type ?u.533961
as : Array α
bs : Array β
f : α → β → γ
i : Nat
hi : i < min as.size bs.size
⊢ i < as.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.533946
β : Type ?u.533949
γ : Type ?u.533961
as : Array α
bs : Array β
f : α → β → γ
i : Nat
hi : i < (zipWith f as bs).size
⊢ i < as.size

Tactic:
simp at hi

Result:
α : Type ?u.533946
β : Type ?u.533949
γ : Type ?u.533961
as : Array α
bs : Array β
f : α → β → γ
i : Nat
hi : i < min as.size bs.size
⊢ i < as.size

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
hi : i < (zipWith f { toList := toList✝¹ } { toList := toList✝ }).size
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ })[i] = f { toList := toList✝¹ }[i] { toList := toList✝ }[i]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : Array α
bs : Array β
f : α → β → γ
i : Nat
hi : i < (zipWith f as bs).size
⊢ (zipWith f as bs)[i] = f as[i] bs[i]

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
bs : Array β
f : α → β → γ
i : Nat
toList✝ : List α
hi : i < (zipWith f { toList := toList✝ } bs).size
⊢ (zipWith f { toList := toList✝ } bs)[i] = f { toList := toList✝ }[i] bs[i]

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
bs : Array β
f : α → β → γ
i : Nat
toList✝ : List α
hi : i < (zipWith f { toList := toList✝ } bs).size
⊢ (zipWith f { toList := toList✝ } bs)[i] = f { toList := toList✝ }[i] bs[i]

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
hi : i < (zipWith f { toList := toList✝¹ } { toList := toList✝ }).size
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ })[i] = f { toList := toList✝¹ }[i] { toList := toList✝ }[i]

Proof state:
α : Type ?u.533946
β : Type ?u.533949
γ : Type ?u.533961
as : Array α
bs : Array β
f : α → β → γ
i : Nat
hi : i < (zipWith f as bs).size
⊢ i < bs.size

Tactic:
simp at hi

Result:
α : Type ?u.533946
β : Type ?u.533949
γ : Type ?u.533961
as : Array α
bs : Array β
f : α → β → γ
i : Nat
hi : i < min as.size bs.size
⊢ i < bs.size

Proof state:
α : Type ?u.533946
β : Type ?u.533949
γ : Type ?u.533961
as : Array α
bs : Array β
f : α → β → γ
i : Nat
hi : i < min as.size bs.size
⊢ i < bs.size

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem lintegral_rpow_enorm_eq_rpow_eLpNorm' {f : α → ε} (hq0_lt : 0 < q) :
    ∫⁻ a, ‖f a‖ₑ ^ q ∂μ = eLpNorm' f q μ ^ q

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq0_lt : 0 < q
⊢ q ≠ 0

Tactic:
exact hq0_lt.ne'

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = eLpNorm' f q μ ^ q

Tactic:
rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div, inv_mul_cancel₀, ENNReal.rpow_one]

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq0_lt : 0 < q
⊢ q ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem msb_neg {w : Nat} {x : BitVec w} :
    (-x).msb = ((x != 0#w && x != intMin w) ^^ x.msb)

Proof state:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
i : Nat
hi : i < w
⊢ x.getMsbD i = (0#w).getMsbD i

Tactic:
simp only [getMsbD_zero]

Result:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
i : Nat
hi : i < w
⊢ x.getMsbD i = false

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Tactic:
suffices ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
  by simp [show x != 0#w by simpa, show x != intMin w by simpa, this]

Result:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
⊢ ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true

Proof state:
case pred.succ
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = decide (n✝ + 1 = 0)

Tactic:
case succ => exact getMsbD_x _ hi (by omega)

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
⊢ x = 0#w

Tactic:
apply eq_of_getMsbD_eq

Result:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
⊢ ∀ (i : Nat), i < w → x.getMsbD i = (0#w).getMsbD i

Proof state:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
⊢ ∀ (i : Nat), i < w → x.getMsbD i = (intMin w).getMsbD i

Tactic:
intro i hi

Result:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
i : Nat
hi : i < w
⊢ x.getMsbD i = (intMin w).getMsbD i

Proof state:
w : Nat
x : BitVec w
⊢ (-x).msb = (x != 0#w && x != intMin w ^^ x.msb)

Tactic:
simp only [BitVec.msb, getMsbD_neg]

Result:
w : Nat
x : BitVec w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Proof state:
w : Nat
x : BitVec w
hmin : x = intMin w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Tactic:
have : (∃ j, j < w ∧ 0 < j ∧ 0 < w ∧ j = 0) ↔ False := by
  simp; omega

Result:
w : Nat
x : BitVec w
hmin : x = intMin w
this : (∃ j, j < w ∧ 0 < j ∧ 0 < w ∧ j = 0) ↔ False
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)
-- Mathlib/CategoryTheory/Closed/Ideal.lean
theorem bijection_natural (A B : C) (X X' : D) (f : (reflector i).obj (A ⊗ B) ⟶ X) (g : X ⟶ X') :
    bijection i _ _ _ (f ≫ g) = bijection i _ _ _ f ≫ g

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.fullyFaithfulOfReflective.preimage
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
        uncurry
            ((unitCompPartialBijective B ⋯)
              (curry
                ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                  uncurry
                      ((unitCompPartialBijective A ⋯)
                        (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          uncurry
              ((unitCompPartialBijective B ⋯)
                (curry
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    uncurry
                        ((unitCompPartialBijective A ⋯)
                          (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g

Tactic:
apply i.map_injective

Result:
case a
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.map
      (i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          uncurry
              ((unitCompPartialBijective B ⋯)
                (curry
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    uncurry
                        ((unitCompPartialBijective A ⋯)
                          (curry
                            ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                      𝟙 (i.obj X')))) ≫
            𝟙 (i.obj X'))) =
    i.map
      (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X)) ≫
        g)
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive]
lemma IsMulFreimanHom.mono (hmn : m ≤ n) (hf : IsMulFreimanHom n A B f) :
    IsMulFreimanHom m A B f where
  mapsTo := hf.mapsTo
  map_prod_eq_map_prod s t hsA htA hs ht h

Proof state:
case inr.intro.refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
h : s.prod = t.prod
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ t ∨ a ∈ replicate (n - m) a✝
⊢ a ∈ A

Tactic:
obtain ha | ha := ha

Result:
case inr.intro.refine_2.inl
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
h : s.prod = t.prod
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ t
⊢ a ∈ A

case inr.intro.refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
h : s.prod = t.prod
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ replicate (n - m) a✝
⊢ a ∈ A

Proof state:
case inr.intro.refine_4
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
h : s.prod = t.prod
a : α
ha : a ∈ A
⊢ (t + replicate (n - m) a).card = n

Tactic:
rw [card_add, card_replicate, ht, Nat.add_sub_cancel' hmn]

Result:
no goals

Proof state:
case inr.intro.refine_1.inr
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
h : s.prod = t.prod
a✝ : α
ha✝ : a✝ ∈ A
a : α
ha : a ∈ replicate (n - m) a✝
⊢ a ∈ A

Tactic:
rwa [eq_of_mem_replicate ha]

Result:
no goals

Proof state:
case inr.intro.refine_5
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
B : Set β
f : α → β
m n : ℕ
hmn : m ≤ n
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = m
ht : t.card = m
h : s.prod = t.prod
a : α
ha : a ∈ A
⊢ (s + replicate (n - m) a).prod = (t + replicate (n - m) a).prod

Tactic:
rw [prod_add, prod_add, h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem condition (a) : I.fst a ≫ K.π (J.fst a) = I.snd a ≫ K.π (J.snd a)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.fst a ≫ K.π (J.fst a) = I.snd a ≫ K.π (J.snd a)

Tactic:
rw [← K.snd_app_right, ← K.fst_app_right]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
lemma isOpen_A_with_param {r s : ℝ} (hf : Continuous f.uncurry) (L : E →L[𝕜] F) :
    IsOpen {p : α × E | p.2 ∈ A (f p.1) L r s}

Proof state:
case mk.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
ha : Continuous (f a)
t : ℝ
hrt : r / 2 < t
htr' : t < r'
⊢ {p |
      ∃ r',
        (r / 2 < r' ∧ r' ≤ r) ∧
          ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈
    𝓝 (a, x)

Tactic:
rcases exists_between hrt with ⟨t', hrt', ht't⟩

Result:
case mk.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
ha : Continuous (f a)
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
⊢ {p |
      ∃ r',
        (r / 2 < r' ∧ r' ≤ r) ∧
          ∀ (y : E), dist y p.2 < r' → ∀ (z : E), dist z p.2 < r' → ‖f p.1 z - f p.1 y - (L z - L y)‖ < s * r} ∈
    𝓝 (a, x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
ha : Continuous (f a)
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
⊢ Continuous fun p => ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖

Tactic:
fun_prop

Result:
no goals